Awais Qasim ¹, Syed Asad Raza Kazmi ¹, Ilyas Fakhir ¹

Affiliations
1 Department of Computer Science, Government College University, Lahore - 5400, PK

Abstract

Background: Software agents are expected to work autonomously and deal with unfamiliar situations astutely. Achieving cent percent test case coverage for these agents has always been a problem due to limited resources. Also a high degree of dependability is expected from autonomous software agents. Formal verification of these systems can be done by specifying the possible actions of the agents to increase the confidence in the correctness of such systems. Methods: We have used social approach of agent communication where actions of the agents are described as social obligation between the participants. Formal specification of e-agents was done using μ-calculus as it is more expressive than Linear Temporal Logic (LTL). An algorithm has been given for syntactic conversion of μ-calculus formulas to TAPA model checker environment. Results: Using converstion algorithm syntactically modified μ-calculus formulas will be executed on TAPA model checker to verify the system being modelled for the specified properties. Application: The study will help to provide future directions for formal modelling of e-agents for their correct functioning.

Keywords

Agent Communication, Model Checking, μ-Calculus, μ TAPA Model Checker

Full Text

   

Ilyas Fakhir ¹, Syed Asad Raza Kazmi ¹, Awais Qasim ¹, Imran Rafique ¹

Affiliations
1 Department of Computer Science, GC University, Lahore – 54000, PK

Abstract

Background: The design of concurrent systems has become more and more articulated during the last three decades, thus forcing radical modifications on the overall methodological approach. In concurrent systems multiple tasks are being performed in parallel, giving rise to nondeterminism in these situations. The goal of this work is to introduce a common formalized framework to improve the shortcomings of existing models of concurrency, most of which use an oversimplified model of time. Methods: In this paper we will model a manufacturing system having concurrent machines by Colored Petri Nets (CPN) technique. For verification of such systems, intuitionistic linear-time μ-calculus (IμTL) will be applied, which is based on Heyting algebra. IμTL is the extension of linear-time μ-calculus. Reasoning about composition in general, but especially concurrent composition, remains one of the greatest challenge. Findings: The IμTL rules will be used for verifying soundness and composition of safety properties, which are more general than previously discussed rules by using Linear-Time Temporal Logic (LTL). These results will also show the verification of concurrent systems using IμTL. Application: This research will provide new direction for modeling and verification of concurrent system.

Keywords

Compositional Reasoning, Concurrent System, CPN, IμTL

Full Text

   

Syed Asad Raza Kazmi ¹, Ayesha Naeem ², Awais Qasim ²

Affiliations
1 Department of Computer Science, Government College University, Lahore,, PK
2 Department of Computer Science, Government College University, Lahore, PK

Abstract

Objectives: In this work, we have introduced a method for formally verifying the concurrent activities of multiple robots. The objective is to formalize a framework for concurrent systems by using temporal logics. Methods/Statistical Analysis: The movement of the robots in given environment is modelled as a weighted transition system and the target is specified in Linear Temporal Logic (LTL) formulae over a set of propositions. Findings: The LTL formulas are characterized to handle the uncertainty or any abnormal activity during the process. The system is designed using SPIN model checker in which different LTL properties are verified. A theoretical description is supported by some experimental results, generated using the existing logics and techniques. Application/ Improvement: This work can be implemented for the surveillance task in pickup and delivery network.

Keywords

Formal Verification, Model Checking, Path Planning, Robotics

Full Text

   

Imran Rafique ¹, Hina Gul ², Salman Rafique ³, Syed Asad Raza Kazmi ¹, Awais Qasim ¹, Ilyas Fakhir ¹

Affiliations
1 Department of Computer Science, GC University, Lahore – 54000, PK
2 Department of Computer Science, Kinnaird College for Women, Lahore– 54000, PK
3 Department of Computer of Science and Engineering, University of Engineering and Technology, Lahore − 54890, PK

Abstract

Objectives: Recent technical advances have fueled the popularity of mobile grid computing. Mobile devices such as cellular phones and PDAs are becoming more common due to the diminution in their size and increase of computational power. In addition, wireless networks are also beginning to fill the environment. With these advances, mobile devices are becoming available to act as service providers in Grid. But the mobile environment presents a number of challenges. Analysis: The range of mobile execution platforms now available which introduces the problem of heterogeneity. Heavy weight checkpoints also provide hindrance to achieve this integration. At present, Grid Computing standards, neither state any load sharing architecture and model that integrates mobile devices in Grid computing nor does it provide any policy that hides heterogeneity and overcome memory limitations of mobile devices thus it is still an open research problem. Findings: Mobile Grid computing solutions must be developed that are lightweight, independent of specific platform and a load sharing model for mobile grid computing that distributes computational tasks on heterogeneous mobile devices. Our simulation results show the effectiveness of data optimization techniques for mobile devices, interoperability and proxy performance in heterogeneous mobile environment. Novelty: We propose a novel layered architecture that adjusts the data size of checkpoints at the minimum possible level and a load sharing Mobile Proxy algorithm.

Keywords

Broker, Checkpointing, Control Flow Graph, Data Liveliness, Heterogeneity, Interoperability, Proxy, Web Service

Full Text

   

Syed Asad Raza Kazmi ¹, Sana Abubakkar ¹, Awais Qasim ¹, Syed Hassan Abbas Kazmi ², Usman Qamar Qureshi ³

Affiliations
1 Department of Computer Science, Government College University, Katchery Road, Lahore – 54000, PK
2 King Edward Medical University, Nelagumbad, Mayo Hospital Road, Lahore – 54000, PK
3 Nishtar Medical College, Multan – 60000, PK

Abstract

Objectives: The importance of error free smooth functioning of the heart pacemaker in providing consistent relief to the heart patients has pushed the researchers to devise highly refined bug free devices. Pacemaker is an important safety critical device that is used to keep the heartbeat uniform in patients with low heartbeat. Since the smooth functioning of the pacemaker is responsible to provide oxygen and nutrients to the whole body of the patient in an appropriate ratio, therefore, any conflict in the device would be life threatening. It is therefore extremely necessary to ensure the error free working of such critical health device. Methods: Previously, different verification methods have been employed to design and verify safety critical devices with varying degree of reliability and reproducibility. Keeping in view the specifications of the pacemaker, this paper presents a model for the verification and validation of a pacemaker system using the SPIN model checker. Findings: The LTL formulas are characterized to handle the uncertainty or any abnormal activity during the process. The system model is designed using SPIN model checker in which different LTL properties are verified. A theoretical description is supported by some experimental results, generated using the existing logics and techniques. Application: This work can be further enhanced for the formal verification of critical medical equipment to ensure their correct functioning.

Keywords

Formal Modelling, Pacemaker Modelling, Pacemaker Systems, Temporal Modelling.

Full Text